A:Type, I:MaInterface(A), i:{i:Id| (i  fpf-domain(I))} . (I(i).2)  a:Knd fp Top 

latex

Definitions	False, t  T, P  Q, A, {x:A| B(x)} , left + right, P  Q, Dec(P), Knd, b, Top, x:AB(x), x:A. B(x), State(ds), Type, x:A  B(x), hasloc(k;i), x. t(x), a:A fp B(a), Id, x.A(x), fpf-domain(f), (x  l), Atom$n, f(x), t.1, t.2, MaInterface(T), P  Q, P & Q, P  Q, IdDeq, x  dom(f), s = t, , a < b, if b then t else f fi , Void, x:A.B(x), True, T
Lemmas	squash wf, true wf, subtype-fpf2, subtype-fpf-variant, pi1 wf, fpf-ap wf, member-fpf-domain, id-deq wf, pi2 wf, l member wf, Id wf, decidable l member, decidable equal Id, fpf-domain wf, fpf-trivial-subtype-top, fpf wf, Knd wf, assert wf, hasloc wf, decl-state wf, top wf